Nuprl Definition : Q-R-glues 11,40

g glues Ia:Qa f Ib:Rb
== {Iag== {Ib} & g is Qa-Rb-pre-preserving on {Ib}
== & Inj({e:E| (e  Ib)} ;E;g)
== & (e:E(Ib). f(g(e)) = Ib(e)) 
latex



clarification:

Q-R-glues(es;Ib_valtype;g;f;Ia;Qa;Ib;Rb)
== weak-antecedent-surjection(es;{Ib};{Ia};g) & Q-R-pre-preserving(es;g;{Ib};Qa;Rb)
== & Inj({e:es-E(es)| (e  Ib)} ;es-E(es);g)
== & (e:es-E-interface(es;Ib). f(g(e)) = Ib(e Ib_valtype
latex


DefinitionsQ f== P, f is Q-R-pre-preserving on P, {I}, P & Q, Inj(A;B;f), {x:AB(x)} , b, e  X, E, x:AB(x), E(X), s = t, f(a), X(e)
FDL editor aliasesQ-R-glues

origin